; <lemma>
;  <title>gen_hotel_new.14</title>
;  <origin>gen_hotel_new | hotel_new_0 | master/inv5/INV</origin>
(benchmark gen_hotel_new_14
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
  :logic AUFLIA
;  <typenv>
;    <variable name="frst" type="INTEGER"/>
;    <variable name="last" type="INTEGER"/>
;  </typenv>
  :extrafuns ((frst Int)
	       (last Int))
  :extramacros (
		 (subseteq
		   (lambda (?p ('t boolean)) (?q ('t boolean)) .
		     (forall (?x 't). 
		       (implies (?p ?x) (?q ?x)))))
		 (subset
		   (lambda (?p ('t boolean)) (?q ('t boolean)) .
		     (and (subseteq ?p ?q)
		       (not (= ?p ?q)))))
		 (range (lambda (?i1 Int) (?i2 Int) .
			  (lambda (?i Int) .
			    (and (<= ?i1 ?i) (<= ?i ?i2)))))
		 )
; <hypothesis needed="true">last &lt; frst</hypothesis>
  :assumption (< last frst)
; <hypothesis needed="true">frst >= 1</hypothesis>
  :assumption (>= frst 1)
; <goal>1 .. last <: 1 .. frst</goal> <-- strict subset -->
  :formula
  (not
    (subset 
      (range 1 last)
      (range 1 frst))
    )
)
; </lemma>

